Search Results

Documents authored by Padoan, Tommaso

Document
DOI: 10.4230/LIPIcs.CSL.2023.7
A Lattice-Theoretical View of Strategy Iteration

Authors: Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of complete lattices, based on MV-chains. We devise algorithms that can be used for non-expansive fixpoint functions represented as so-called min- respectively max-decompositions. Correspondingly, we develop two different techniques: strategy iteration from above, which has to solve the problem that iteration might reach a fixpoint that is not the least, and from below, which is algorithmically simpler, but requires a more involved correctness argument. We apply our method to solve energy games and compute behavioural metrics for probabilistic automata.
Cite as

Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. A Lattice-Theoretical View of Strategy Iteration. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CSL.2023.7,
  author =	{Baldan, Paolo and Eggert, Richard and K\"{o}nig, Barbara and Padoan, Tommaso},
  title =	{{A Lattice-Theoretical View of Strategy Iteration}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.7},
  URN =		{urn:nbn:de:0030-drops-174680},
  doi =		{10.4230/LIPIcs.CSL.2023.7},
  annote =	{Keywords: games, strategy iteration, fixpoints, energy games, behavioural metrics}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.13
(Un)Decidability for History Preserving True Concurrent Logics

Authors: Paolo Baldan, Alberto Carraro, and Tommaso Padoan

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We investigate the satisfiability problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal (in)dependencies. Variants of such logics have been studied, with different expressiveness, corresponding to a number of true concurrent behavioural equivalences. Here we focus on a mu-calculus style logic that represents the counterpart of history-preserving (hp-)bisimilarity, a typical equivalence in the true concurrent spectrum of bisimilarities. It is known that one can decide whether or not two 1-safe Petri nets (and in general finite asynchronous transition systems) are hp-bisimilar. Moreover, for the logic that captures hp-bisimilarity the model-checking problem is decidable with respect to prime event structures satisfying suitable regularity conditions. To the best of our knowledge, the problem of satisfiability has been scarcely investigated in the realm of true concurrent logics. We show that satisfiability for the logic for hp-bisimilarity is undecidable via a reduction from domino tilings. The fragment of the logic without fixpoints, instead, turns out to be decidable. We consider these results a first step towards a more complete investigation of the satisfiability problem for true concurrent logics, which we believe to have notable solvable cases.
Cite as

Paolo Baldan, Alberto Carraro, and Tommaso Padoan. (Un)Decidability for History Preserving True Concurrent Logics. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.MFCS.2021.13,
  author =	{Baldan, Paolo and Carraro, Alberto and Padoan, Tommaso},
  title =	{{(Un)Decidability for History Preserving True Concurrent Logics}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.13},
  URN =		{urn:nbn:de:0030-drops-144532},
  doi =		{10.4230/LIPIcs.MFCS.2021.13},
  annote =	{Keywords: Event structures, history-preserving bisimilarity, true concurrent behavioural logics, satisfiability, decidability, domino systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.25
Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations

Authors: Paolo Baldan, Barbara König, and Tommaso Padoan

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express many verification tasks such as model-checking of various kinds of specification logics or the check of coinductive behavioural equivalences. In this paper we develop a theory of approximation for systems of fixpoint equations in the style of abstract interpretation: a system over some concrete domain is abstracted to a system in a suitable abstract domain, with conditions ensuring that the abstract solution represents a sound/complete overapproximation of the concrete solution. Interestingly, up-to techniques, a classical approach used in coinductive settings to obtain easier or feasible proofs, can be interpreted as abstractions in a way that they naturally fit into our framework and extend to systems of equations. Additionally, relying on the approximation theory, we can characterise the solution of systems of fixpoint equations over complete lattices in terms of a suitable parity game, generalising some recent work that was restricted to continuous lattices. The game view opens the way for the development of local algorithms for characterising the solution of such equation systems and we explore some special cases.
Cite as

Paolo Baldan, Barbara König, and Tommaso Padoan. Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CONCUR.2020.25,
  author =	{Baldan, Paolo and K\"{o}nig, Barbara and Padoan, Tommaso},
  title =	{{Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.25},
  URN =		{urn:nbn:de:0030-drops-128373},
  doi =		{10.4230/LIPIcs.CONCUR.2020.25},
  annote =	{Keywords: fixpoint equation systems, complete lattices, parity games, abstract interpretation, up-to techniques, \mu-calculus, bisimilarity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact